Inference at * 2 
Iof proof for Lemma p-mu-exists:



1. P : 
2. (n:. ((P(n))))
  x: + Top. p-mu(P;x) 

latex

 by (InstConcl [inr  ]) 
CollapseTHEN ((Auto) 
CollapseTHEN ((UnfoldTopAb 0) 
CollapseTHEN ((
CReduce 0) 
CollapseTHEN ((Auto) 
CollapseTHEN ((ParallelOp ( -2)) 
CollapseTHEN ((InstConcl [
Ci]) 
CollapseTHEN (Auto))))))) 

latex

C.

Definitions	inr x , , p-mu(P;x), , {x:A| B(x)} , , A  B, Void, x:AB(x), A, P  Q, False, x:A. B(x), b, x:A. B(x), f(a), t  T
Lemmas	assert wf